00100	These notes are intended to provide a basis for answering Licklider's
00200	questions about when and how work on MTC and automatic programming
00300	and formal reasoning will pay off.
00400	
00500	1. Each of these areas has a pure research component for which a day
00600	of payoff cannot presently be predicted, but there is a predictable
00700	payoff for some of it.  Probably the above should be said so that we
00800	don't get into the position of having to justify the immediate payoff
00900	of every detail, but it should be said more softly and probably not
01000	first.
01100	
01200	2. Proving programs correct will require one or more new programming
01300	languages.  The practical programmers will find the anomalies of
01400	existing languages (it is necessary to document the anomalies, and
01500	this could best be done in reference to the IBM Vienna formalization
01600	of PL/I) even more inconvenient in proving practical programs than
01700	logicians find it in proving example programs.  The definition of
01800	such languages must wait until the verification of enough different
01900	types of programs has been carried far enough so that we know what
02000	we need. (References to the different types of programs that have
02100	been verified here and elsewhere should be made and the need to
02200	co-ordinate this work should be stated.  Perhaps there should be an
02300	ARPA sponsored conference on making program verification a practical
02400	tool.).
02500